f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), a) → F(x, g(a))
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), a) → F(x, g(a))
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(g(x), a) → F(x, g(a))
Used ordering: Polynomial interpretation [25,35]:
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), g(y)) → H(g(y), x, g(y))
The value of delta used in the strict ordering is 21/2.
POL(a) = 7/2
POL(g(x1)) = (1/4)x_1
POL(h(x1, x2, x3)) = x_3
POL(f(x1, x2)) = x_2
POL(F(x1, x2)) = (4)x_2
POL(H(x1, x2, x3)) = (4)x_3
f(a, g(y)) → g(g(y))
h(g(x), y, z) → f(y, h(x, y, z))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(g(x), g(y)) → H(g(y), x, g(y))
Used ordering: Polynomial interpretation [25,35]:
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
The value of delta used in the strict ordering is 1/4.
POL(a) = 0
POL(g(x1)) = 1 + (4)x_1
POL(h(x1, x2, x3)) = 4 + (3/2)x_1 + (2)x_2
POL(f(x1, x2)) = 1/4 + (13/4)x_1 + (1/2)x_2
POL(F(x1, x2)) = 3/4 + (1/4)x_1
POL(H(x1, x2, x3)) = 3/4 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → H(x, y, z)
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(g(x), y, z) → H(x, y, z)
The value of delta used in the strict ordering is 4.
POL(g(x1)) = 1 + (4)x_1
POL(H(x1, x2, x3)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z